structure Prfgen2 =
struct
  structure P = Proof2
  structure Asm = Assem
  structure A = Assert
  structure S2A = Svc2avc2
  structure T = Temp
  structure Tr = Transp
  structure LCoq = LCoqize2
  structure R = A_Reduce
  structure DP = DebugPrint

  fun mapToAddr (id) = 0 (* cheat compiler! *)
  fun reg2exp(reg) = 
      let fun handlereg(Asm.Eax) = A.Eax
	    | handlereg(Asm.Ebx) = A.Ebx
	    | handlereg(Asm.Ecx) = A.Ecx
	    | handlereg(Asm.Edx) = A.Edx
	    | handlereg(Asm.Esi) = A.Esi
	    | handlereg(Asm.Edi) = A.Edi
	    | handlereg(Asm.Esp) = A.Esp
	    | handlereg(Asm.Ebp) = A.Ebp
      in handlereg(reg)
      end

(* update State: state*instr-> state *)
  fun upState instr st= 
      let fun rf(state:A.state) = #1 state
	  fun hp(state:A.state) = #2 state
	  fun mchinstr(Asm.Addr(r1,r2)) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Addz(imm,r2)) = 
	      let val updexp2 = A.Plus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Subr(r1,r2)) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Subz(imm,r2)) = 
	      let val updexp2 = A.Minus(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Mulr(r1,r2)) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.Sel(rf(st),reg2exp(r1)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Mulz(imm,r2)) = 
	      let val updexp2 = A.Times(A.Sel(rf(st),reg2exp(r2)),
				       A.IntNum(imm))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp2),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Push(r1)) = 
	      let val rfupdexp2 = A.Minus(A.Sel(rf(st),A.Esp),A.IntNum(4))
		  val rf' = A.Upd(rf(st),A.Esp,rfupdexp2)
		  (* may cause some mistake here *)
		  (*val hp' = A.Upd(hp(st),A.Sel(rf(st),A.Esp),
				  A.Sel(rf(st),reg2exp(r1)))*)
		  val hp' = A.Upd(hp(st),A.Sel(rf',A.Esp),
				  A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf',hp')
	      in st'
	      end
	    | mchinstr(Asm.Pop(r1)) = 
	      let val updesp = A.Upd(rf(st), A.Esp,
				     A.Plus(A.Sel(rf(st),A.Esp),A.IntNum(4)))
		  val rf' = A.Upd(updesp,reg2exp(r1),
				  A.Sel(hp(st),A.Sel(rf(st),A.Esp)))
		  val st' = (rf',hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Xchg(r1,r2)) = 
	      let val rf1 = A.Upd(rf(st),reg2exp(r1),A.Sel(rf(st),reg2exp(r2)))
		  val st' = (A.Upd(rf1,reg2exp(r2),A.Sel(rf(st),reg2exp(r1))),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Leal(str,r1)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r1),A.Addr(mapToAddr(str))),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Leab(ofaddr,r1,r2)) = (*WIP*)
	      let val addr = A.Plus(A.Sel(rf(st),reg2exp(r1)),
				    A.IntNum(ofaddr))
		  val st' = (A.Upd(rf(st),reg2exp(r2),addr),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movr(r1,r2)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.Sel(rf(st),reg2exp(r1)))
			     ,hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movz(imm,r2)) = 
	      let val st' = (A.Upd(rf(st),reg2exp(r2),A.IntNum(imm)),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movld(imm,r1,r2)) = 
	      let val updexp1 = A.Sel(hp(st),A.Plus(A.Sel(rf(st),reg2exp(r1)),
						    A.IntNum(imm)))
		  val st' = (A.Upd(rf(st),reg2exp(r2),updexp1),hp(st))
	      in st'
	      end
	    | mchinstr(Asm.Movst(r1,imm,r2)) = 
	      let val updexp1 = A.Plus(A.Sel(rf(st),reg2exp(r2)),A.IntNum(imm))
		  val hp' = A.Upd(hp(st),updexp1,A.Sel(rf(st),reg2exp(r1)))
		  val st' = (rf(st),hp')
	      in st'
	      end
            | mchinstr(Asm.Ret) =
              let val rf' = A.Upd(rf(st), A.Esp,
				 A.Plus(A.Sel(rf(st),A.Esp),A.IntNum(4)))
                  val st' = (rf', hp(st))
              in  st'
              end
	    | mchinstr(_) = st
      in mchinstr(instr)
      end

  fun upspec specs l a = 
      let fun up [] = []
            | up ({lab=l', asst=a'}::spec) = if l=l'
                                             then {lab=l, asst=a}::(up spec)
                                             else {lab=l', asst=a'}:: (up spec)
      in  specs := up (!specs)
      end

  (* generate the proof of a code block that has precondition *)
  fun prf_gen (cd_b, prf_b) post cb specs lab = 
      let fun gen ((Asm.Jmp(l))::cb') =
              let val postopt = A.getspec l (!specs)
                  val post' = case (postopt)
                              (* WIP : should raise fail *)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val st = upState (Asm.Jmp(l))
                  val a = (fn st_init:A.state => post' (st st_init)) 
              in  case cb'
                   of  [] => ([Asm.Jmp(l)], lab, P.WF_jmp (l, lab))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_jmp (l,"")
                                val new_cd_b = [Asm.Jmp(l)]
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen (Asm.Ret :: cb') = (* Work In Progress *)
              let (*get post condition*)
                  val postopt = A.getspec "post_condition" (!specs)
                  val post' = case postopt
                              of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                (* (print ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True)) *)
                                | SOME(a) => a
                  (* generate a *)
                  val st = upState (Asm.Ret)
                  val a = (fn st_init:A.state => post' (st st_init)) 
              in  case cb'
                   of  [] => ([Asm.Ret], lab, P.WF_trivial)  (*WIP*)
                     | _  => let val new_asst = T.new_asst lab
                                 val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                 val new_prf_b = P.WF_trivial (*WIP*)
                                 val new_cd_b = [Asm.Ret]
                             in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                             end
              end
            | gen ((Asm.Bgt(r1, r2, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r1' = reg2exp r1
                  val r2' = reg2exp r2
                  val a = (fn st:A.state => A.And(A.Imply(A.Gt(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post1 st), 
                                                  A.Imply(A.Le(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post2 st))) 
              in  case cb'
                   of  [] => ((Asm.Bgt(r1,r2,l))::cd_b, lab, P.WF_bgt (l, prf_b, post, lab))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_bgt (l, prf_b, post, "")
                                val new_cd_b = (Asm.Bgt(r1,r2, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Bgti(i, r, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r' = reg2exp r
                  val i' = A.IntNum(i)
                  val a = (fn st:A.state => A.And(A.Imply(A.Gt(i', A.Sel(#1 st, r')), post1 st), 
                                                  A.Imply(A.Le(i', A.Sel(#1 st, r')), post2 st))) 
              in  case cb'
                   of  [] => ((Asm.Bgti(i,r,l))::cd_b, lab, P.WF_bgti (l, prf_b, post, lab))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_bgti (l, prf_b, post, "")
                                val new_cd_b = (Asm.Bgti(i,r, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Bge(r1, r2, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r1' = reg2exp r1
                  val r2' = reg2exp r2
                  val a = (fn st:A.state => A.And(A.Imply(A.Ge(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post1 st), 
                                                  A.Imply(A.Lt(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post2 st))) 
              in  case cb'
                   of  [] => ((Asm.Bge(r1,r2,l))::cd_b, lab, P.WF_bge (l, prf_b, post, lab))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_bge (l, prf_b, post, "")
                                val new_cd_b = (Asm.Bge(r1,r2, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Beq(r1, r2, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r1' = reg2exp r1
                  val r2' = reg2exp r2
                  val a = (fn st:A.state => A.And(A.Imply(A.Eq(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post1 st), 
                                                  A.Imply(A.Ne(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post2 st))) 
              in  case cb'
                   of  [] => ((Asm.Beq(r1,r2,l))::cd_b, lab, P.WF_beq (l, prf_b, post, lab))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_beq (l, prf_b, post, "")
                                val new_cd_b = (Asm.Beq(r1,r2, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Beqi(i, r, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r' = reg2exp r
                  val i' = A.IntNum(i)
                  val a = (fn st:A.state => A.And(A.Imply(A.Eq(i', A.Sel(#1 st, r')), post1 st), 
                                                  A.Imply(A.Ne(i', A.Sel(#1 st, r')), post2 st))) 
              in  case cb'
                   of  [] => ((Asm.Beqi(i,r,l))::cd_b, lab, P.WF_beqi (l, prf_b, post, lab))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_beqi (l, prf_b, post, "")
                                val new_cd_b = (Asm.Beqi(i,r, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Addr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Addr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Addr(r1,r2))::cd_b, lab ,(P.WF_addr (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_addr (prf_b, post, "") 
                                val new_cd_b = (Asm.Addr(r1,r2))::cd_b                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Addz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Addz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>((Asm.Addz(i,r))::cd_b, lab ,(P.WF_addz (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_addz (prf_b, post, "") 
                                val new_cd_b = (Asm.Addz(i,r))::cd_b                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Subr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Subr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Addr(r1,r2))::cd_b, lab ,(P.WF_subr (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst =(SOME a)} :: (!specs)
                                val new_prf_b = P.WF_subr (prf_b, post, "") 
                                val new_cd_b = (Asm.Subr(r1,r2))::cd_b                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Subz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Subz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>((Asm.Subz(i,r))::cd_b, lab ,(P.WF_subz (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_subz (prf_b, post, "") 
                                val new_cd_b = (Asm.Subz(i,r))::cd_b                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Mulr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Mulr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Mulr(r1,r2))::cd_b, lab ,(P.WF_mulr (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_mulr (prf_b, post, "") 
                                val new_cd_b = (Asm.Mulr(r1,r2))::cd_b                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Mulz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Mulz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>((Asm.Mulz(i,r))::cd_b, lab ,(P.WF_mulz (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_mulz (prf_b, post, "") 
                                val new_cd_b = (Asm.Mulz(i,r))::cd_b                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Movr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Movr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Movr(r1,r2))::cd_b, lab ,(P.WF_movr (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_movr (prf_b, post, "") 
                                val new_cd_b = (Asm.Movr(r1,r2))::cd_b                                                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Movld(i, r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Movld(i, r1,r2))
                  val n = T.new_var()
                  val a = (fn st_init:A.state => 
                                   (A.And(A.InDom(A.Plus(A.IntNum(i), A.Sel(#1 st_init, reg2exp r1)), #2 st_init), post' (st st_init))))
              in  case cb'
                   of  [] => ((Asm.Movld(i, r1,r2))::cd_b, lab ,(P.WF_movld (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_movld (prf_b, post, "") 
                                val new_cd_b = (Asm.Movld(i, r1,r2))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Movst(r1, i, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Movst(r1, i,r2))
                  val n = T.new_var()
                  val a = (fn st_init:A.state => 
                                   (A.And(A.InDom(A.Plus(A.IntNum(i), A.Sel(#1 st_init, reg2exp r2)), #2 st_init), post' (st st_init))))
              in  case cb'
                   of  [] => ((Asm.Movst(r1, i, r2))::cd_b, lab ,(P.WF_movst (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_movst (prf_b, post, "") 
                                val new_cd_b = (Asm.Movst(r1, i, r2))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end


            | gen ((Asm.Movz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Movz(i, r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Movz(i, r))::cd_b, lab ,(P.WF_movz (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_movz (prf_b, post, "") 
                                val new_cd_b = (Asm.Movz(i,r))::cd_b                                                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Push r)::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Push r)
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Push r)::cd_b, lab,(P.WF_push (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs)
                                val new_prf_b = P.WF_push (prf_b, post, "") 
                                val new_cd_b = (Asm.Push r)::cd_b                                
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            (* WIP should raise Fail *)

            | gen ((Asm.Pop r)::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Pop r)
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Pop r)::cd_b, lab,(P.WF_pop (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst =(SOME a)} :: (!specs)
                                val new_prf_b = P.WF_pop (prf_b, post, "") 
                                val new_cd_b = (Asm.Pop r)::cd_b                                
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Xchg(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Xchg(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] => ((Asm.Xchg(r1,r2))::cd_b, lab ,(P.WF_xchg (prf_b, post, lab)))
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst =(SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_xchg (prf_b, post, "") 
                                val new_cd_b = (Asm.Xchg(r1,r2))::cd_b                                                               
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.ExtraAsst(a))::cb') = 
              let val postopt = A.getspec post (!specs)
                  val post' = case postopt
                               of NONE => (raise Fail ("Impossible! No such label: "^post); (fn st:A.state=>A.True))
                                | SOME(a') => a'
                  val a' = (fn st_init:A.state => A.And(post' st_init, a st_init)) 
              in  case cb'
                   of  [] => let val preopt = A.getspec lab (!specs)  (*WIP: is it right?*)
                                 val pre' = case preopt
                                             of NONE => (raise Fail ("Impossible! No such label: "^lab); (fn st:A.state=>A.True))
                                              | SOME(a)=>a
                                 val pre = (fn st_init:A.state => A.And(pre' st_init, a st_init))
                                 val _ = upspec specs lab (SOME pre)                              
                             in  (cd_b, lab, prf_b)
                             end
                     | _ => let val _ = upspec specs post (SOME a')
                            in  prf_gen (cd_b, prf_b) post cb' specs lab
                            end
              end
            | gen (i::cb') = (DP.print_asm i; raise Fail "work in progress!\n"; (i::cd_b, "bogus", P.WF_trivial))
            | gen [] = (raise Fail "impossible!"; (cd_b, "bogus", P.WF_trivial))
      in  gen cb
      end


  (* generate the proof of the current instructions in current code block, 
   * because that the current code block has no pre-condition,
   * this function also generate a precondition for it
   *
   * (cb_b, ass, prf_b): sub-proof of current code block which can be used in generating current instructions proof.
   *                     this cb_b is in positive order.
   * post: post condition of the current instruction
   * cb: current instructions, in negative order.
   * specs: real specifications
   * lab: label of current code block, it is used to insert generated pre-condition of the current code block
   *)
  fun prf_gen_no_pre (cd_b, prf_b) post cb specs lab = 
      let
          fun gen ((Asm.Jmp(l))::cb') =
              let (* get current post-condition *)
                  val postopt = A.getspec l (!specs)
                  val post' = case postopt
                              (* WIP: should raise Fail *)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                (* (print ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True)) *)
                                | SOME(a) => a
                  (*generate pre-condition "a" of the current instruction *)
                  val st = upState (Asm.Jmp(l))
                  val a = (fn st_init:A.state => post' (st st_init)) 
              in  case cb'
                   of  [] => (*if the code block has only a jmp instruction, then a is the precondition of the code block*)
                             let val _ = upspec specs lab (SOME a)
                             in  (* return the proof: code block, pre-condition, proof-term*)
                                 ([Asm.Jmp l], lab, P.WF_jmp (l,""))
                             end
                     | _ => (* if the code block has other instructions, then packed the current proof as a sub-proof
                             * of the hole code block's proof. and continue to generate other sub-proof.*)
                            let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs))
                                val new_prf_b = P.WF_jmp (l, "")
                                val new_cd_b = [Asm.Jmp l] 
                                val _ = print ("code = jmp; label = "^lab^"\n")                           
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end

            | gen (Asm.Ret :: cb') = (* Work In Progress *)
              let (*get post condition*)
                  val postopt = A.getspec "post_condition" (!specs)
                  val post = case postopt
                              (* WIP: should raise Fail *)
                              of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                (* (print ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True)) *)
                                | SOME(a) => a
                  (* generate a *)
                  val st = upState (Asm.Ret)
                  val a = (fn st_init:A.state => post (st st_init)) 
              in  case cb'
                   of  [] => let val _ = upspec specs lab (SOME a) 
                                 val _ = print ("code = ret; label = "^lab^"\n")
                             in ([Asm.Ret], lab, P.WF_trivial)  (*WIP*)
                             end
                     | _  => let val new_asst = T.new_asst lab
                                 val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs))
                                 val new_prf_b = P.WF_trivial (*WIP*)
                                 val new_cd_b = [Asm.Ret] 
                                 val _ = print ("code = ret; label = "^lab^"\n")                               
                             in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                             end
              end
            | gen ((Asm.Bgt(r1, r2, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r1' = reg2exp r1
                  val r2' = reg2exp r2
                  val a = (fn st:A.state => A.And(A.Imply(A.Gt(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post1 st), 
                                                  A.Imply(A.Le(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post2 st))) 
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  ((Asm.Bgt(r1,r2,l))::cd_b, lab, P.WF_bgt (l, prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_bgt (l, prf_b, post, "")
                                val new_cd_b = (Asm.Bgt(r1,r2, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Bgti(i, r, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val i' = A.IntNum(i)
                  val r' = reg2exp r
                  val a = (fn st:A.state => A.And(A.Imply(A.Gt(i', A.Sel(#1 st, r')), post1 st), 
                                                  A.Imply(A.Le(i', A.Sel(#1 st, r')), post2 st))) 
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a)  
                              in  ((Asm.Bgti(i,r,l))::cd_b, lab, P.WF_bgti (l, prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_bgti (l, prf_b, post, "")
                                val new_cd_b = (Asm.Bgti(i,r, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Bge(r1, r2, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r1' = reg2exp r1
                  val r2' = reg2exp r2
                  val a = (fn st:A.state => A.And(A.Imply(A.Ge(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post1 st), 
                                                  A.Imply(A.Lt(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post2 st))) 
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  ((Asm.Bge(r1,r2,l))::cd_b, lab, P.WF_bge (l, prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst = (SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_bge (l, prf_b, post, "")
                                val new_cd_b = (Asm.Bge(r1,r2, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Beqi(i, r, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val i' = A.IntNum(i)
                  val r' = reg2exp r
                  val a = (fn st:A.state => A.And(A.Imply(A.Eq(i', A.Sel(#1 st, r')), post1 st), 
                                                  A.Imply(A.Ne(i', A.Sel(#1 st, r')), post2 st))) 
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  ((Asm.Beqi(i,r,l))::cd_b, lab, P.WF_beqi (l, prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst =(SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_beqi (l, prf_b, post, "")
                                val new_cd_b = (Asm.Beqi(i,r, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Beq(r1, r2, l))::cb') =
              let val postopt1 = A.getspec l (!specs)
                  val post1 = case (postopt1)
                              of  NONE => (raise Fail ("Impossible! No such label: "^l^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val postopt2 = A.getspec post (!specs)
                  val post2 = case (postopt2)
                              of  NONE => (raise Fail ("Impossible! No such label: "^post^"\n"); (fn st:A.state => A.True))
                                | SOME(a) => a
                  val r1' = reg2exp r1
                  val r2' = reg2exp r2
                  val a = (fn st:A.state => A.And(A.Imply(A.Eq(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post1 st), 
                                                  A.Imply(A.Ne(A.Sel(#1 st, r1'), A.Sel(#1 st, r2')), post2 st))) 
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  ((Asm.Beq(r1,r2,l))::cd_b, lab, P.WF_beq (l, prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = specs := {lab=new_asst, asst =(SOME a)} :: (!specs) 
                                val new_prf_b = P.WF_beq (l, prf_b, post, "")
                                val new_cd_b = (Asm.Beq(r1,r2, l))::cd_b
                            in  prf_gen (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end 
              end
            | gen ((Asm.Addr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Addr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in (((Asm.Addr (r1, r2))::cd_b), lab, P.WF_addr (prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs))
                                val new_prf_b = P.WF_addr (prf_b, post, "")
                                val new_cd_b = (Asm.Addr (r1, r2))::cd_b                                
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Addz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Addz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a)     
                                  val _ = print ("code = addz; pre_label = "^lab^"\n") 
                              in  (((Asm.Addz (i, r))::cd_b), lab, P.WF_addz (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_addz (prf_b, post, "")
                                val new_cd_b = (Asm.Addz (i, r))::cd_b 
                                val _ = print ("code = addz; label = "^lab^"\n")                                
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Subr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Subr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in (((Asm.Subr (r1, r2))::cd_b), lab, P.WF_subr (prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_subr (prf_b, post, "")
                                val new_cd_b = (Asm.Subr (r1, r2))::cd_b                                
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Subz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Subz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  (((Asm.Subz (i, r))::cd_b), lab, P.WF_subz (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_subz (prf_b, post, "")
                                val new_cd_b = (Asm.Subz (i, r))::cd_b                                 
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Mulr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Mulr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in (((Asm.Mulr (r1, r2))::cd_b), lab, P.WF_mulr (prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_mulr (prf_b, post, "")
                                val new_cd_b = (Asm.Mulr (r1, r2))::cd_b                                
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Mulz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Mulz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  (((Asm.Mulz (i, r))::cd_b), lab, P.WF_mulz (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_mulz (prf_b, post, "")
                                val new_cd_b = (Asm.Mulz (i, r))::cd_b                                 
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Movr(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Movr(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a)  
                                  val _ = print ("code = movr; pre_label = "^lab^"\n")
                              in (((Asm.Movr (r1, r2))::cd_b), lab, P.WF_movr (prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs))
                                val new_prf_b = P.WF_movr (prf_b, post, "")
                                val new_cd_b = (Asm.Movr (r1, r2))::cd_b 
                                val _ = print ("code = movr; label = "^lab^"\n")                              
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Movld(i, r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val n = T.new_var()
                  val st = upState (Asm.Movld(i, r1, r2))
                  val a = (fn st_init:A.state =>  
                                   (A.And(A.InDom(A.Plus(A.IntNum(i), A.Sel(#1 st_init, reg2exp r1)), #2 st_init), post' (st st_init))))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a)  
                              in  (((Asm.Movld (i, r1, r2))::cd_b), lab, P.WF_movld (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs)) 
                                val new_prf_b = P.WF_movld (prf_b, post, "")
                                val new_cd_b = (Asm.Movld (i, r1, r2))::cd_b 
                                val _ = print ("code = movld; label = "^lab^"\n")                              
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Movst(r1, i, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val n = T.new_var()
                  val st = upState (Asm.Movst(r1, i, r2))
                  val a = (fn st_init:A.state =>  
                                   (A.And(A.InDom(A.Plus(A.IntNum(i), A.Sel(#1 st_init, reg2exp r2)), #2 st_init), post' (st st_init))))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in  (((Asm.Movst (r1, i, r2))::cd_b), lab, P.WF_movst (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs)) 
                                val new_prf_b = P.WF_movst (prf_b, post, "")
                                val new_cd_b = (Asm.Movst (r1, i, r2))::cd_b                                
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end

            | gen ((Asm.Movz(i, r))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Movz(i,r))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in (((Asm.Movz (i, r))::cd_b), lab, P.WF_movz (prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs))
                                val new_prf_b = P.WF_movz (prf_b, post, "")
                                val new_cd_b = (Asm.Movz (i, r))::cd_b                               
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Push r)::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a 
                  val st = upState (Asm.Push r)
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in (((Asm.Push r)::cd_b), lab, P.WF_push (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_push (prf_b, post, "")
                                val new_cd_b = (Asm.Push r)::cd_b                               
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Pop r)::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a 
                  val st = upState (Asm.Pop r)
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                                  val _ = print ("code = pop; label = "^lab^"\n")
                             in (((Asm.Pop r)::cd_b), lab, P.WF_pop (prf_b, post, ""))
                             end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst = (SOME a)} :: (!specs))
                                val new_prf_b = P.WF_pop (prf_b, post, "")
                                val new_cd_b = (Asm.Pop r)::cd_b  
                                val _ = print ("code = pop; label = "^lab^"\n")                             
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.Xchg(r1, r2))::cb') =
              let val postopt = A.getspec post (!specs)
                  val post' =  case postopt
                                of  NONE => (raise Fail ("Impossible! No such label: post_condition \n"); (fn st:A.state => A.True))
                                  | SOME(a) => a
                  val st = upState (Asm.Xchg(r1,r2))
                  val a = (fn st_init:A.state => post' (st st_init))
              in  case cb'
                   of  [] =>  let val _ = upspec specs lab (SOME a) 
                              in (((Asm.Xchg (r1, r2))::cd_b), lab, P.WF_xchg (prf_b, post, ""))
                              end
                     | _ => let val new_asst = T.new_asst lab
                                val _ = (specs := {lab=new_asst, asst =(SOME a)} :: (!specs))
                                val new_prf_b = P.WF_xchg (prf_b, post, "")
                                val new_cd_b = (Asm.Xchg (r1, r2))::cd_b                               
                            in  prf_gen_no_pre (new_cd_b, new_prf_b) new_asst cb' specs lab
                            end
              end
            | gen ((Asm.ExtraAsst(a))::cb') = 
              let val postopt = A.getspec post (!specs)
                  val post' = case postopt
                               of NONE => (raise Fail ("Impossible! No such label: "^post); (fn st:A.state=>A.True))
                                | SOME(a') => a'
                  val a' = (fn st_init:A.state => A.And(post' st_init, a st_init)) 
              in  case cb'
                   of  [] => let val _ = upspec specs lab (SOME a')
                             in  (cd_b, lab, prf_b)
                             end
                     | _ => let val _ = upspec specs post (SOME a')
                            in  prf_gen_no_pre (cd_b, prf_b) post cb' specs lab
                            end
              end
            | gen (i::cb') = (print "work in progress!\n"; (i::cd_b, "bogus", P.WF_trivial)) (*WIP*)
            | gen [] = (raise Fail "impossible!"; (cd_b, "bogus", P.WF_trivial))
      in  gen cb
      end

  (* get the code block which is marked by lab in the code list,
   * NOTICE: the generate code block is in negative order.  
   * lab: label, mark the current code block 
   * code: all the assembly code list (positive order)
   *)
  fun get_cb code lab =
      let (* get the start of the code block *)
          fun getlab [] = (raise Fail "no such lab in codes!"; [])
            | getlab ((Asm.Label(l, a))::code') = if (l = lab)
                                                  then code'
                                                  else getlab code'
            | getlab (_::code') = getlab code'
          val begin = getlab code
          val cb = ref []
          (* from the start of the code block to find the end of the code block,
           * generate the current code block that in negative order
           *)
          fun get [] = (raise Fail ("there is no instruction?");())
            | get (Asm.Label(l,_)::code') = (raise Fail ("should not meet a label: "^l); ())
            | get (Asm.Section(_)::code') = (raise Fail ("should not meet a section");())
            | get ((Asm.Jmp l) :: code') = (cb := (Asm.Jmp l) ::(!cb))
            | get (Asm.Call f :: code') = (cb := (Asm.Call f) :: (!cb))
            | get (Asm.Ret :: code') = (cb := (Asm.Ret)::(!cb))
            | get (i::code') = (cb := i::(!cb); (get code'))
      in  get begin;
          !(cb)
      end

  (* generate all the proof of the code block whose labels are in the spec_index, and
   * also generate every code blocks' pre-conditions.
   *
   * spec_index: labels that has no specification, 
   * code: positive order assembly code (all the code)
   * specs: real specification (current all specification)
   *)
  fun prf_list_gen_1 spec_index code specs =
      let val prf_list = ref [] (* proof list *)
          (* generate all the proof of the code blocks whose label is in the the arguments label list *)
          fun gen (l::speci) = 
              let val cb = get_cb code l (* get current code block (negative order)*)
                  fun nogood ((Asm.Jmp l1)::cb') = 
                      if List.exists (fn x => x=l1) (l::speci)
                      then true
                      else nogood cb'
                    | nogood (Asm.Ret :: cb') =
                      if List.exists (fn x => x="post_condition") (l::speci)
                      then true
                      else nogood cb'
                    | nogood ((Asm.Bgt(r1, r2, l1))::cb') =
                      if List.exists (fn x => x = l1) (l::speci)
                      then true
                      else nogood cb'
                    | nogood ((Asm.Bge(r1, r2, l1))::cb') =
                      if List.exists (fn x => x = l1) (l::speci)
                      then true
                      else nogood cb'
                    | nogood ((Asm.Beq(r1, r2, l1))::cb') =
                      if List.exists (fn x => x = l1) (l::speci)
                      then true
                      else nogood cb'
                    | nogood ((Asm.Bgti(i, r, l1))::cb') =
                      if List.exists (fn x => x = l1) (l::speci)
                      then true
                      else nogood cb'
                    | nogood ((Asm.Beqi(i, r, l1))::cb') =
                      if List.exists (fn x => x = l1) (l::speci)
                      then true
                      else nogood cb'
                    | nogood (_::cb') = nogood cb'
                    | nogood [] = false
              in  (* if the post-condition's label has no real specification, then put the code block in the tail
                   * of the processing list and pick another code block to process 
                   *)
                  if nogood cb
                  then (gen (speci@[l]))
                  else let val _ = T.reset_asst()
                           (* generate the proof and precondition of the code block *)
                           val proof = prf_gen_no_pre ([], P.WF_trivial) "bogus" cb specs l
                       in  prf_list := ((l, proof):: !prf_list); (* put proof and its label into the proof list *)
                           gen speci (*continue to generate other code block's proof until the speci is empty *)
                       end
              end
            | gen [] = ()
      in  gen spec_index; (* generate all the code blocks' proof in the spec_index *)
          !prf_list (* return the proof list*)
      end

  fun prf_list_gen_2 spec_index code specs =
      let val prf_list = ref []
          fun gen (l::speci) = 
              let val cb = get_cb code l
(*
                  val l1 = case cb 
                            of (Asm.Jmp(l2)::cb') => l2
                             | (Asm.Ret::cb')=> "post_condition" 
                             | _ => (raise Fail "impossible, last instruction is not a jmp!\n"; "bogus") 
*)
              in  let val _ = T.reset_asst()
                      val proof = prf_gen ([], P.WF_trivial) "bogus" cb specs l
                  in  prf_list := ((l, proof):: !prf_list);
                      gen speci
                  end
              end
            | gen [] = ()
      in  gen spec_index;
          !prf_list
      end

 (* fun lookupct_prf_gen (spec_name, spec) l a1 = P.True *)
  fun lookupct_prf_gen (spec_name, spec) l a1 =  (* WIP *)
      let (* the following also can be seperated in some tactics *)
	  fun nullemit str:string = str
	  val ct = List.map (fn (str_spec, lic) => (str_spec^"_asst", lic)) spec
	  val newl = String.map LCoq.filt l (*substite . to _ in label's name*)
	  (* lookup corresponding label number *)
	  val lnum' = case (LCoq.lkup spec newl)
		       of SOME(l') => l'
			| NONE => (raise Fail "There is no such label!"; 0)
	  val a1' = newl^"_asst"
(*	  fun hd_eq ict il ia = 
	      let val ict' = LCoq.pr_chty 0 nullemit ict (* WIP *)
		  val s_il = Int.toString(il)
	      in P.App(P.App(P.App(P.Var("lookupCT_eq"),P.Var(ict')),P.Var(s_il)),P.Var(ia))
	      end*)
	  fun hd_eq ift il ia = [P.T_apply("lookupCT_eq", [])]
(*	  fun hd_neq ict il il' ia ia' pchild = 
	      let val ict' = LCoq.pr_chty 0 nullemit ict  (* WIP *)
		  val s_il = Int.toString(il)
		  val s_il' = Int.toString(il')
		  val pchild' = (*P.Ne(P.IntNum(il),P.IntNum(il'))*)
		      let val sub_prf = (fn true => "(fun H : "^ s_il ^" = "^ s_il'^ "=>\n"^
						    "let H0 := eq_ind (Zpos ("^s_il^"-"^s_il'^"))\n"^
						    "(fun ee : Z => match ee with \n"^
						    "| Z0 => False \n | Zpos _ => True \n | Zneg _ => False \n end)"^
						    " I 0%Z (Zegal_left "^s_il^" "^s_il'^" (inj_eq "^s_il^" "^s_il'^"H)) in \n "^
						    "False_ind False H0)"
					  | false => "(fun H : "^ s_il ^" = "^ s_il'^ "=>\n"^
						     "let H0 := eq_ind (Zneg ("^s_il'^"-"^s_il^"))\n"^
						     "(fun ee : Z => match ee with \n"^
						     "| Z0 => False \n | Zpos _ => False \n | Zneg _ => True \n end)"^
						     " I 0%Z (Zegal_left "^s_il^" "^s_il'^" (inj_eq "^s_il^" "^s_il'^"H)) in \n "^
						     "False_ind False H0)") (il > il')
		      in P.Var(sub_prf)
		      end
	      in P.App(P.App(P.App(P.App(P.App(P.App(P.App(P.Var("lookupCT_neq"),P.Var(ict')),
						     P.Var(s_il)),
					       P.Var(s_il')),
					 P.Var(ia)),
				   P.Var(ia')),
			     pchild),
		       pchild')
	      end*)
	  fun hd_neq ict il il' ia ia' pchild = 
	      (P.T_auto) :: (pchild @ [P.T_apply("lookupCT_neq", [])])
	  fun wk_ct lic' s_a ((s_spec, lic):: ls) = if lic = lic' 
						    then hd_eq ls lic' s_a
						    else (let val p_child = wk_ct lic' s_a ls 
							  in hd_neq ls lic lic' s_spec s_a p_child
							  end
							      )
	    | wk_ct lic' s_a [] = [P.T_exact(P.True)] (*WIP*) 
      in wk_ct lnum' a1' ct
      end

  val Current_Hty : string ref = ref ""
  (* translated proof into simple typed lambda calculus style. 
   *
   * prf: the proof to be translated.
   * (spec_name, spec): the specification list's name and the specification index list
   * env: variable environment
   * senv: structure type environment
   *)
  fun prf_blk_gen a prf (spec_name, spec, specs) env senv =
      let fun ppp (P.WF_addr(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                      if lemma = ""
                      then let val tmp_var = T.new_var()
                               val alist = "R"::"H"::[tmp_var]
                               val n1 = T.new_var()
                               val n2 = T.new_var()
                               val alist2 = n1::[n2]
                           in  P.T_or(P.T_apply(tmp_var, []), 
                                      P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                               [P.T_intros alist]
                           end
                      else let val lemma' = String.map LCoq.filt lemma
                               val tac1 = P.T_apply("Asst_"^lemma', [])
                               val I = T.new_var()
                               val e = T.new_var()
                               val ne = T.new_var()
                               val alist1 = [e]
                               val alist2 =[ne]
                               val alist3 = ["R", "H", I]
                               val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                               val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                               val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                               val tac2 = P.T_seq(P.T_intros alist3, 
                                                  P.T_seq(P.T_split,
                                                          P.T_seq(P.T_para taclist1,
                                                                  P.T_seq(P.T_para taclist2, 
                                                                          P.T_para taclist3)))) 
                           in  [P.T_or(tac1, tac2)]
                           end
              in  sub_prf1 @ sub_prf2@[P.T_apply ("I_add", [("a'", a1)])]
              end
            | ppp (P.WF_addz(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var] 
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
              in sub_prf1 @ sub_prf2 @[P.T_apply ("I_addi", [("a'", a1)])]
              end  
            | ppp (P.WF_subr(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                      if lemma = ""
                      then let val tmp_var = T.new_var()
                               val alist = "R"::"H"::[tmp_var]
                               val n1 = T.new_var()
                               val n2 = T.new_var()
                               val alist2 = n1::[n2]
                           in  P.T_or(P.T_apply(tmp_var, []), 
                                      P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                               [P.T_intros alist]
                           end
                      else let val lemma' = String.map LCoq.filt lemma
                               val tac1 = P.T_apply("Asst_"^lemma', [])
                               val I = T.new_var()
                               val e = T.new_var()
                               val ne = T.new_var()
                               val alist1 = [e]
                               val alist2 =[ne]
                               val alist3 = ["R", "H", I]
                               val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                               val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                               val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                               val tac2 = P.T_seq(P.T_intros alist3, 
                                                  P.T_seq(P.T_split,
                                                          P.T_seq(P.T_para taclist1,
                                                                  P.T_seq(P.T_para taclist2, 
                                                                          P.T_para taclist3)))) 
                           in  [P.T_or(tac1, tac2)]
                           end
              in  sub_prf1 @ sub_prf2@[P.T_apply ("I_sub", [("a'", a1)])]
              end
            | ppp (P.WF_subz(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
              in sub_prf1 @ sub_prf2 @[P.T_apply ("I_subi", [("a'", a1)])]
              end
            | ppp (P.WF_mulr(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                      if lemma = ""
                      then let val tmp_var = T.new_var()
                               val alist = "R"::"H"::[tmp_var]
                               val n1 = T.new_var()
                               val n2 = T.new_var()
                               val alist2 = n1::[n2]
                           in  P.T_or(P.T_apply(tmp_var, []), 
                                      P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                               [P.T_intros alist]
                           end
                      else let val lemma' = String.map LCoq.filt lemma
                               val tac1 = P.T_apply("Asst_"^lemma', [])
                               val I = T.new_var()
                               val e = T.new_var()
                               val ne = T.new_var()
                               val alist1 = [e]
                               val alist2 =[ne]
                               val alist3 = ["R", "H", I]
                               val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                               val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                               val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                               val tac2 = P.T_seq(P.T_intros alist3, 
                                                  P.T_seq(P.T_split,
                                                          P.T_seq(P.T_para taclist1,
                                                                  P.T_seq(P.T_para taclist2, 
                                                                          P.T_para taclist3)))) 
                           in  [P.T_or(tac1, tac2)]
                           end
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_mul", [("a'", a1)])]
              end
            | ppp (P.WF_mulz(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
              in sub_prf1 @ sub_prf2 @[P.T_apply ("I_muli", [("a'", a1)])]
              end 
            | ppp (P.WF_movr(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
                                    (*  let val lemma' = String.map LCoq.filt lemma
                                        in  [P.T_apply("Asst_"^lemma', [])]
                                        end *)
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_mov", [("a'", a1)])]
              end
            | ppp (P.WF_movld(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                      in  [P.T_apply("Asst_"^lemma', [])]
                                      end
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_movld", [("a'", a1)])]
              end   
            | ppp (P.WF_movst(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_movst", [("a'", a1)])]
              end  
            | ppp (P.WF_movz(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_movi", [("a'", a1)])]
              end 
            | ppp (P.WF_xchg(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                      if lemma = ""
                      then let val tmp_var = T.new_var()
                               val alist = "R"::"H"::[tmp_var]
                               val n1 = T.new_var()
                               val n2 = T.new_var()
                               val alist2 = n1::[n2]
                           in  P.T_or(P.T_apply(tmp_var, []), 
                                      P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                               [P.T_intros alist]
                           end
                      else let val lemma' = String.map LCoq.filt lemma
                               val tac1 = P.T_apply("Asst_"^lemma', [])
                               val I = T.new_var()
                               val e = T.new_var()
                               val ne = T.new_var()
                               val alist1 = [e]
                               val alist2 =[ne]
                               val alist3 = ["R", "H", I]
                               val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                               val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                               val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                               val tac2 = P.T_seq(P.T_intros alist3, 
                                                  P.T_seq(P.T_split,
                                                          P.T_seq(P.T_para taclist1,
                                                                  P.T_seq(P.T_para taclist2, 
                                                                          P.T_para taclist3)))) 
                           in  [P.T_or(tac1, tac2)]
                           end
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_xchg", [("a'", a1)])]
              end 
            | ppp (P.WF_push(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                 if lemma = ""
                                 then let val tmp_var = T.new_var()
                                          val alist = "R"::"H"::[tmp_var]
                                          val n1 = T.new_var()
                                          val n2 = T.new_var()
                                          val alist2 = n1::[n2]
                                      in  P.T_or(P.T_apply(tmp_var, []), 
                                                 P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                          [P.T_intros alist]
                                      end
                                 else let val lemma' = String.map LCoq.filt lemma
                                          val tac1 = P.T_apply("Asst_"^lemma', [])
                                          val I = T.new_var()
                                          val e = T.new_var()
                                          val ne = T.new_var()
                                          val alist1 = [e]
                                          val alist2 =[ne]
                                          val alist3 = ["R", "H", I]
                                          val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                          val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                          val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                          val tac2 = P.T_seq(P.T_intros alist3, 
                                                             P.T_seq(P.T_split,
                                                                     P.T_seq(P.T_para taclist1,
                                                                             P.T_seq(P.T_para taclist2, 
                                                                                     P.T_para taclist3)))) 
                                      in  [P.T_or(tac1, tac2)]
                                      end
              in sub_prf1 @ sub_prf2 @[P.T_apply ("I_push", [("a'", a1)])]
              end
            | ppp (P.WF_pop(prf1, a1, lemma)) =
              let val sub_prf1 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv (* Psi |- {a} I *)
                  val sub_prf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                      if lemma = ""
                      then let val tmp_var = T.new_var()
                               val alist = "R"::"H"::[tmp_var]
                               val n1 = T.new_var()
                               val n2 = T.new_var()
                               val alist2 = n1::[n2]
                           in  P.T_or(P.T_apply(tmp_var, []), 
                                      P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                               [P.T_intros alist]
                           end
                      else let val lemma' = String.map LCoq.filt lemma
                               val tac1 = P.T_apply("Asst_"^lemma', [])
                               val I = T.new_var()
                               val e = T.new_var()
                               val ne = T.new_var()
                               val alist1 = [e]
                               val alist2 =[ne]
                               val alist3 = ["R", "H", I]
                               val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                               val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                               val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                               val tac2 = P.T_seq(P.T_intros alist3, 
                                                  P.T_seq(P.T_split,
                                                          P.T_seq(P.T_para taclist1,
                                                                  P.T_seq(P.T_para taclist2, 
                                                                          P.T_para taclist3)))) 
                           in  [P.T_or(tac1, tac2)]
                           end
              in  sub_prf1 @ sub_prf2 @ [P.T_apply ("I_pop", [("a'", a1)])]
              end
            | ppp (P.WF_jmp (l, lemma)) =
              let val ra1' = A.getspec l specs
                  val ra1 =  case (ra1')
                              of  NONE => (raise Fail ("Impossible! No such precondition: "^l^"\n"); 
                                           (fn st:A.state => A.True))
                                | SOME(a) => a
(*                  val subprf1 = P.T_exact(lookupct_prf_gen (spec_name, spec) l ra1) (* Psi(l) = a1 *)*)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l ra1 (* Psi(l) = a1 *)
                  val subprf2 = (* if has no vc, then generate it and its proof, else using vc to generate proof *)
                                if lemma = ""
                                then let val tmp_var = T.new_var()
                                         val alist = "R" :: "H" ::[tmp_var]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val alist2 = n1::[n2]
                                     in  P.T_or(P.T_apply(tmp_var, []), 
                                                P.T_seq(P.T_inversion_clear(tmp_var, alist2), P.T_apply(n1, [])))::
                                         [P.T_intros alist]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val tac1 = P.T_apply("Asst_"^lemma', [])
                                         val I = T.new_var()
                                         val e = T.new_var()
                                         val ne = T.new_var()
                                         val alist1 = [e]
                                         val alist2 =[ne]
                                         val alist3 = ["R", "H", I]
                                         val taclist1 = [P.T_intros alist1, P.T_intros alist2]
                                         val taclist2 = [P.T_apply("Asst_"^lemma'^"_e",[]), P.T_apply("Asst_"^lemma'^"_ne", [])]
                                         val taclist3 = [P.T_apply(I,[]), P.T_apply(e, []), P.T_apply(I, []), P.T_apply(ne, [])]
                                         val tac2 = P.T_seq(P.T_intros alist3, 
                                                            P.T_seq(P.T_split,
                                                                    P.T_seq(P.T_para taclist1,
                                                                            P.T_seq(P.T_para taclist2, 
                                                                                    P.T_para taclist3)))) 
                                     in  [P.T_or(tac1, tac2)]
                                     end
              in  subprf2 @ subprf1@[P.T_unfold(!Current_Hty),P.T_apply("I_jmp",[("a1", l)])]
              end
            | ppp (P.WF_bgt(l, prf1, a1, lemma)) =
              let val ra1' = A.getspec l specs
                  val ra1 = case (ra1')
                              of  NONE => (raise Fail ("Impossible! No such precondition: "^l^"\n"); 
                                           (fn st:A.state => A.True))
                                | SOME(a) => a
(*                  val subprf1 = P.T_exact(lookupct_prf_gen (spec_name, spec) l ra1)*)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l ra1
                  val subprf2 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = n1::n2::[n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n2, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2),
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val ne = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", ne, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(ne, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_ne",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val subprf3 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n1, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2),
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val e = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", e, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(e, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_e",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val sub_prf4 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv
              in  sub_prf4 @ subprf3 @ subprf2 @subprf1@[P.T_unfold(!Current_Hty),P.T_apply("I_bgt", [("a'",a1), ("a1",l)])]
              end
            | ppp (P.WF_bge(l, prf1, a1, lemma)) =
              let val ra1' = A.getspec l specs
                  val ra1 = case (ra1')
                              of  NONE => (raise Fail ("Impossible! No such precondition: "^l^"\n"); 
                                           (fn st:A.state => A.True))
                                | SOME(a) => a
(*                  val subprf1 = P.T_exact(lookupct_prf_gen (spec_name, spec) l ra1)*)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l ra1
                  val subprf2 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n2, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2),
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val ne = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", ne, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(ne, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_ne",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val subprf3 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n1, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2),
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val e = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", e, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(e, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_e",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val sub_prf4 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv
              in  sub_prf4 @ subprf3 @ subprf2 @subprf1@[P.T_unfold(!Current_Hty),P.T_apply("I_bge", [("a'",a1), ("a1",l)])]
              end
            | ppp (P.WF_beq(l, prf1, a1, lemma)) =
              let val ra1' = A.getspec l specs
                  val ra1 = case (ra1')
                              of  NONE => (raise Fail ("Impossible! No such precondition: "^l^"\n"); 
                                           (fn st:A.state => A.True))
                                | SOME(a) => a
(*                  val subprf1 = P.T_exact(lookupct_prf_gen (spec_name, spec) l ra1)*)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l ra1
                  val subprf2 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n2, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2), 
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val ne = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", ne, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(ne, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_ne",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val subprf3 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n1, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2),
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val e = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", e, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(e, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_e",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val sub_prf4 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv
              in  sub_prf4 @ subprf3 @ subprf2 @subprf1@[P.T_unfold(!Current_Hty),P.T_apply("I_beq", [("a'",a1), ("a1",l)])]
              end
            | ppp (P.WF_bgti(l, prf1, a1, lemma)) =
              let val ra1' = A.getspec l specs
                  val ra1 = case (ra1')
                              of  NONE => (raise Fail ("Impossible! No such precondition: "^l^"\n"); 
                                           (fn st:A.state => A.True))
                                | SOME(a) => a
(*                  val subprf1 = P.T_exact(lookupct_prf_gen (spec_name, spec) l ra1)*)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l ra1
                  val subprf2 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n2, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2), 
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val ne = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", ne, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(ne, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_ne",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val subprf3 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n1, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2),
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val e = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", e, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(e, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_e",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val sub_prf4 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv
              in  sub_prf4 @ subprf3 @ subprf2 @subprf1@[P.T_unfold(!Current_Hty),P.T_apply("I_bgti", [("a'",a1), ("a1",l)])]
              end
            | ppp (P.WF_beqi(l, prf1, a1, lemma)) =
              let val ra1' = A.getspec l specs
                  val ra1 = case (ra1')
                              of  NONE => (raise Fail ("Impossible! No such precondition: "^l^"\n"); 
                                           (fn st:A.state => A.True))
                                | SOME(a) => a
(*                  val subprf1 = P.T_exact(lookupct_prf_gen (spec_name, spec) l ra1)*)
                  val subprf1 = lookupct_prf_gen (spec_name, spec) l ra1
                  val subprf2 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n2, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2), 
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val ne = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", ne, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(ne, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_ne",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val subprf3 = if lemma = ""
                                then let val tmp_var1 = T.new_var()
                                         val tmp_var2 = T.new_var()
                                         val alist1 =  ["R", "H", tmp_var1, tmp_var2]
                                         val n1 = T.new_var()
                                         val n2 = T.new_var()
                                         val n3 = T.new_var()
                                         val alist2 = n1::[n2]
                                         val alist3 = [n1, n2, n3]
                                     in  (P.T_apply(tmp_var1, []))::
                                         (P.T_apply(n1, []))::
                                         (P.T_or(P.T_inversion_clear(tmp_var2, alist2), 
                                                 P.T_inversion_clear(tmp_var2, alist3)))::
                                         [P.T_intros alist1]
                                     end
                                else let val lemma' = String.map LCoq.filt lemma
                                         val e = T.new_var()
                                         val I = T.new_var()
                                         val alist1 = ["R", "H", e, I]
                                         val paralist = [P.T_apply(I,[]), P.T_apply(e, [])]
                                         val tac1 = P.T_seq(P.T_intros alist1, 
                                                            P.T_seq(P.T_apply("Asst_"^lemma'^"_e",[]), 
                                                                    P.T_para paralist)) 
                                     in  [tac1]
                                     end
                  val sub_prf4 = prf_blk_gen a1 prf1 (spec_name, spec, specs) env senv
              in  sub_prf4 @ subprf3 @ subprf2 @subprf1@[P.T_unfold(!Current_Hty),P.T_apply("I_beqi", [("a'",a1), ("a1",l)])]
              end
            | ppp _ = [P.T_exact(P.True)] (*WIP*) 
      in ppp prf
      end

  (* generate well-formedness lemma 
   *
   * cb: current code block, in positive order.
   * spec_name: the specification list's name
   * a: the pre-condition of the current code block
   *)
  fun lemma_gen cb spec_name a=
      let val codeheapty = P.Var(spec_name)  (*code heap type*)
          val infer_name = P.Var("Infer") (*inference rule name*)
          val is = P.Iseq(cb)  (*code block*)
          val a' = P.Asst(a)   (* pre-condition*)
      in P.App(P.App(P.App(infer_name,codeheapty),a'), is)  (* Psi |- {a} is  *)
      end


  (* generate lemma and proof of a code block's well-formedness.
   *
   * env: variable enironment
   * senv: structure type environment 
   * spec_name: specification list's name
   * spec: specification index list
   * lab: the code block's lab
   * cb: the code block's code
   * a: the pre-condition of the code block
   * prf: the proof of the well-formedness lemma.
   *)
  fun gen_wf_lemma env senv (spec_name, spec, specs) (lab, (cb, a, prf)) =
      let (* generate well-formedness lemma *)
          val lemma = lemma_gen cb spec_name a
          (* generate proof of the lemma *)
          val proof = P.T_proof :: ((List.rev (prf_blk_gen a prf (spec_name, spec, specs) env senv)) @ [P.T_qed])
      in  (lab, lemma, proof)  (*return (lab, lemma, proof)*)
      end

end
